#include "StepByStep.h"

// New Method for Absolute Obstructive
#define NEWABS

void ModifyTreeOfAction();

PCOfLaw *CopyPCOfDomainLaw(DomainLaw *law)
{
  PCOfLaw *PC, *PC1, *PC2, *PC3;

  PC = NULL;
  for (PC1 = law->PC; PC1 != NULL; PC1 = PC1->next) {
    PC2 = (PCOfLaw *) calloc(1, sizeof(PCOfLaw));
    PC2->Not = PC1->Not;
    PC2->Pred = CopyTokenList(PC1->Pred);

    if (PC == NULL) PC = PC2;
    else PC3->next = PC2;

    PC3 = PC2;
  }

  return PC;
}

Bool PCInPCofDomainLaw(PredKnowledge *Pd, TypedList *Para, DomainLaw *law)
{
  TokenList *Pt;
  TypedList *Pt1, *Para1, *Para2;
  PCOfLaw   *PC;
  Bool      Equal;
  int       i, k, Num;

  Num = NumParaOfPred(law->Pred2->VList.ParaIdx);

  Para2 = law->Para;
  for (PC = law->PC; PC != NULL; PC = PC->next) {
    if (Pd->PredNo != PC->Pred->VList.ParaIdx) continue;

    Equal = TRUE;
    Para1 = Para;    Pt1 = Pd->Para;
    for (Pt = PC->Pred->next; Equal && Pt!=NULL; Para1++,Pt=Pt->next) {
      i = Pt->VList.ParaIdx;
      k = Pt1->VList.ParaIdx;

      if (IsConstant(k) || IsConstant(i)) Equal = (k == i);
      else if (Para1->VList.ParaIdx == Para2[i].VList.ParaIdx) Equal = TRUE;
      else Equal = (Para1->VList.NumValue==Para2[i].VList.NumValue && Para2[i].VList.ParaIdx>=Num);
    }

    if (Equal) return TRUE;
  }

  return FALSE;
 }

Bool EqualEffectAndPred(TypedList *Para1, TokenList *Pred1, TypedList *Para2, TokenList *Pred2)
{
  int i, j;

  if (Pred1->VList.ParaIdx != Pred2->VList.ParaIdx) return FALSE;

  Pred2 = Pred2->next;
  for (Pred1 = Pred1->next; Pred1 != NULL; Pred1=Pred1->next,Pred2=Pred2->next) {
    i = Pred1->VList.ParaIdx;
    j = Pred2->VList.ParaIdx;

    if (IsConstant(i) || IsConstant(j)) {
       if (i != j) break;
    }
    else if (Para1[i].VList.ParaIdx != Para2[j].VList.ParaIdx) break;
  }

  return (Pred1 == NULL);
}

void TransDomainLaw(DomainLaw *law)
{
  TypedList *Para;
  int       i;

  Para = law->Para;
  for (i = 0; i < law->NumPara; i++,Para++)
    if (Para->VList.NumValue != 1) {
       Para->VList.Name[0] = 'x';
       Para->VList.Name[1] = '1' + i;
       Para->VList.Name[2] = 0;
    }
}

void IncreaseOneParaOfLaw(DomainLaw *law, TypedList *NewPara)
{
  TypedList *Pt;
  int       Num;

  Num = law->NumPara++;
  law->Para = (TypedList *) realloc(law->Para, (Num+1)*sizeof(TypedList));
  Pt = law->Para + Num;
  Pt->VList.List = NULL;
  CopyOneTypedList(Pt, NewPara);
  Pt->VList.ParaIdx = Num;
}

void IncreaseParaForLaw0_1(int *Para1, DomainLaw *law, TypedList *Para, TokenList *Pred)
{
  TokenList *Pt;
  int	     j, k, Num;

  Num = law->NumPara;
  for (Pt = Pred->next; Pt != NULL; Pt = Pt->next) {
    j  = Pt->VList.ParaIdx;

    if (IsConstant(j)) continue;

    k = (Para+j)->VList.ParaIdx;
    if (Para1[k] != NOFOUND) Pt->VList.ParaIdx = Para1[k];
    else {
           IncreaseOneParaOfLaw(law, Para+j);
           Para1[k] = Pt->VList.ParaIdx = Num++;
    }
  }
}

void IncreaseParaForLaw01(DomainLaw *law, TypedList *PPara, int *APara, TokenList *Pred)
{
  TokenList *Pt;
  int	    i, j, Num;

  Num = law->NumPara;
  for (Pt = Pred->next; Pt != NULL; Pt = Pt->next) {
    j = Pt->VList.ParaIdx;

    if (IsConstant(j)) continue;

    i = APara[j];
    if (i != NOFOUND) Pt->VList.ParaIdx = i;
    else {
           IncreaseOneParaOfLaw(law, PPara+j);
           APara[j] = Pt->VList.ParaIdx = Num++;
    }
  }
}

TokenList* CopyPredIntoTokenList(PredKnowledge *Pd)
{
  TokenList *Pt, *Pt1, *Pt2;
  TypedList *Para;
  int       i, Num;

  Pt = Pt1 = (TokenList *) calloc(1, sizeof(TokenList));
  Pt1->VList.ParaIdx = Pd->PredNo;
  strcpy(Pt1->VList.Name, NameOfPred(Pd->PredNo));

  Num = NumParaOfPred(Pd->PredNo);
  Para = Pd->Para;
  for (i = 0; i < Num; i++,Para++) {
    Pt2 = (TokenList *) calloc(1, sizeof(TokenList));

    Pt2->VList.ParaIdx = Para->VList.ParaIdx;
    strcpy(Pt2->VList.Name, Para->VList.Name);
    CopyValueList(&(Pt2->VList), &(Para->VList));

    Pt1->next = Pt2;  Pt1 = Pt2;
  }

  return Pt;
}

void CopyVarParaOfPredIntoParaOfLaw(DomainLaw *law, PredKnowledge *Pd)
{
  TypedList *Pt, *Pt1, *Para;
  int       i, Num, Num1;

  Pt = Pd->Para;  Num = NumParaOfPred(Pd->PredNo);

  Num1 = 0;   Para = NULL;
  for (i = 0; i < Num; i++,Pt++)
    if (Pt->VList.NumValue != 1) {
       Num1++;
       Para = (TypedList *) realloc(Para, Num1*sizeof(TypedList));
       Pt1 = Para + (Num1-1);
       Pt1->VList.List = NULL;
       CopyOneTypedList(Pt1, Pt);
    }

  law->NumPara = Num1;  law->Para = Para;
}

Bool PredInEffectAction(PredKnowledge *Pd, TypedList *APara, PENode *PE)
{
  TypedList *Para;
  TokenList *Pt;
  Bool      Ok;
  int       idx;

  Ok = (Pd->Type==PE->Type && Pd->PredNo==PE->Pred->VList.ParaIdx);

  Para = Pd->Para;
  for (Pt = PE->Pred->next; Ok && Pt!=NULL; Para++,Pt=Pt->next) {
    idx = Pt->VList.ParaIdx;
    if (!IsConstant(idx)) {
       idx = (APara+idx)->VList.ParaIdx;
       idx = (Pd->Para+idx)->VList.ParaIdx;
    }
    Ok = (idx == Para->VList.ParaIdx);
  }

  return Ok;
}

Bool EqualTwoPreds(TypedList *Para1, TokenList *Pd1, int Num, int *Para2, TokenList *Pd2)
{
  int i, j;

  if (Pd1 == NULL) return TRUE;

  Pd1 = Pd1->next;  Pd2 = Pd2->next;

  while (Pd1 != NULL) {
    i = Pd1->VList.ParaIdx;
    j = Pd2->VList.ParaIdx;
    if (IsConstant(i) || IsConstant(j)) {
       if (i != j) return FALSE;
    }
    else {
           i = (Para1+i)->VList.ParaIdx;
           if (Para2[j] == NOFOUND) {
              if (!CheckTransform(Num, Para2, j, i)) return FALSE;
           }
           else if (Para2[j] != i) return FALSE;
    }

    Pd1 = Pd1->next;  Pd2 = Pd2->next;
  }

  return TRUE;
}

Bool PCListINPCList(TypedList *Para1, PCOfLaw *ListPC1, int Num, int *Para, PCOfLaw *FirstPC, PCOfLaw *ListPC2)
{
  TokenList *Pt1, *Pt2;
  PCOfLaw   *PC2;
  Bool      Ok;
  int       i, j, *OldPara;

  if (ListPC1 == NULL) return TRUE;

  OldPara = (int *) calloc(Num, sizeof(int));

  for (i = 0; i < Num; i++) OldPara[i] = Para[i];

  for (PC2 = FirstPC; PC2 != NULL; PC2 = PC2->next) {
    if (PC2->Not != ListPC1->Not ||
       PC2->Pred->VList.ParaIdx != ListPC1->Pred->VList.ParaIdx) continue;

    Pt1 = ListPC1->Pred->next;
    Pt2 = PC2->Pred->next;
    while (Pt1 != NULL) {
      i = Pt1->VList.ParaIdx;
      j = Pt2->VList.ParaIdx;

      if (IsConstant(i) || IsConstant(j)) {
         if (i != j) break;
      }
      else {
             i = Para1[i].VList.ParaIdx;
             if (Para[j] == NOFOUND) {
                if (!CheckTransform(Num, Para, j, i)) break;
             }
             else if (Para[j] != i) break;
      }

      Pt1 = Pt1->next;  Pt2 = Pt2->next;
    }

    if (Pt1 == NULL) break;
  }

  if (PC2 == NULL) { free(OldPara);  return FALSE; }

  if (PCListINPCList(Para1, ListPC1->next, Num, Para, ListPC2, ListPC2)) {
     free(OldPara);
     return TRUE;
  }

  Ok = PCListINPCList(Para1, ListPC1, Num, OldPara, PC2->next, ListPC2);
  free(OldPara);

  return Ok;
}

DomainLaw *FindLawInListOfDomainLaw(DomainLaw *law, DomainLaw *LAW)
{
  DomainLaw *law1;
  TypedList *Para1, *Para2;
//TokenList *Pt1, *Pt2;
  int       i, PdNo1, PdNo2, Num, *Para;
  PCOfLaw   *Pt1, *Pt2;

//fprintf(Output, "\n"); PrintOneDomainLaw(law);
  PdNo1 = law->Pred1->VList.ParaIdx;
  PdNo2 = law->Pred2->VList.ParaIdx;

  Num = law->NumPara;
  Para = (int *) calloc(Num, sizeof(int));

  Pt1 = law->PCLaw;
  for (law1 = LAW; law1 != NULL; law1 = law1->next) {
    if (law1->Not1!=law->Not1 || law1->Pred1->VList.ParaIdx!=PdNo1 ||
        law1->Not2!=law->Not2 || law1->Pred2->VList.ParaIdx!=PdNo2) continue;

//fprintf(Output, "\n"); PrintOneDomainLaw(law1);

    if (Typing) {
       Para1 = law->Para;
       Para2 = law1->Para;
       for (i = 0; i < Num; i++)
         if (!IsSame(Para1->Type->Name, Para2->Type->Name)) break;

       if (i < Num) continue;
    }

    Pt2 = law1->PCLaw;
    if ((Pt1!=NULL && Pt2==NULL) || (Pt1==NULL && Pt2!=NULL)) continue;

    for (i = 0; i < Num; i++) Para[i] = NOFOUND;
    if (EqualTwoPreds(law1->Para, law1->Pred1, Num, Para, law->Pred1) &&
        EqualTwoPreds(law1->Para, law1->Pred2, Num, Para, law->Pred2) &&
        PCListINPCList(law1->Para, Pt1, Num, Para, Pt2, Pt2) &&
        PCListINPCList(law1->Para, law1->PC, Num, Para, law->PC, law->PC))
       break;
  }

  free(Para);

  return law1;
}

void GetPCListOfLaw(int *Para1, DomainLaw *law, TypedList *Para2, PredKnowledge *PkPC)
{
  TypedList *Pt;
  PCOfLaw   *PC, *PC1;
  int       i, Num;

  PC = NULL;
  while (PkPC != NULL) {
    Num = NumParaOfPred(PkPC->PredNo);

    Pt = PkPC->Para;
    for (i = 0; i < Num; i++,Pt++)
      if (Para1[Pt->VList.ParaIdx] != NOFOUND) break;

    if (Num == 0 || i < Num) {
       PC1 = (PCOfLaw *) calloc(1, sizeof(PCOfLaw));

       PC1->Not = PkPC->Type;
       PC1->Pred = CopyPredIntoTokenList(PkPC);
       IncreaseParaForLaw0_1(Para1, law, Para2, PC1->Pred);

       if (PC == NULL) law->PCLaw = PC1;
       else PC->next = PC1;

       PC = PC1;
    }

    PkPC = PkPC->next;
  }
}

//law: Pd ============> PE
//        (not Pd)^Pc
DomainLaw *AddOneCondRelation(PredKnowledge *PCLaw, PredKnowledge *Pd, ActKnowledge *ActK, PredKnowledge *PC, PENode *PE)
{
  DomainLaw *law, *law1;
  TypedList *Pt2;
  PCOfLaw   *PC1;
  int       i, Num, Num1, *Para;

  Num = NumParaOfPred(Pd->PredNo);
  Num1 = NumParaOfAct(ActK->ActNo);
  Para = (int *) calloc(Num1, sizeof(int));

  law = (DomainLaw *) calloc(1, sizeof(DomainLaw));

  law->Step = 1;
  law->Flag = LAW01;

  law->Not1 = Pd->Type;
  law->Pred1 = CopyPredIntoTokenList(Pd);
  law->Not2 = PE->Type;
  law->Pred2 = CopyTokenList(PE->Pred);

  CopyVarParaOfPredIntoParaOfLaw(law, Pd);

  Pt2 = ActK->Para;
  for (i = 0; i < Num1; i++,Pt2++)
    Para[i] = (Pt2->VList.ParaIdx < Num ? Pt2->VList.ParaIdx : NOFOUND);

  IncreaseParaForLaw01(law, ActK->Para, Para, law->Pred2);

  GetPCListOfLaw(Para, law, Pd->Para, PCLaw);

  PC1 = (PCOfLaw *) calloc(1, sizeof(PCOfLaw));
  PC1->Not = PC->Type;
  PC1->Pred = CopyPredIntoTokenList(PC);
  IncreaseParaForLaw01(law, ActK->Para, Para, PC1->Pred);

  PC1->next = law->PCLaw;
  law->PCLaw = PC1;

  free(Para);

  TransDomainLaw(law);
//fprintf(Output, "\n"); PrintOneDomainLaw(law);

  law1 = FindLawInListOfDomainLaw(law, Law0);
  if (law1 != NULL) {
     FreeDomainOneLaw(law);
     return law1;
  }

#ifdef TEST
  law->Index = (Law0==NULL ? 1 : 1+TLaw0->Index);
#endif
  if (Law0 == NULL) Law0 = law;
  else TLaw0->next = law;

  TLaw0 = law;
  return law;
}

void GetDomainBasicLaw(PKTree *Pk)
{
  PredKnowledge *PC, *Pd, *PkPC;
  ActKnowledge  *ActK;
  DomainLaw     *law;
  TypedList     *Pt;
  TokenList     *Pt1;
  PENode        *PE;
  int	        i, Num, PredNo, *Para;

  PkPC = Pk->PC;  Pd = Pk->Pred;
//PrintPKTree(Pk);

  if (IsType(Pd->Character, CHARACTER))
     for (ActK = Pd->Act; ActK != NULL; ActK = ActK->next)
       for (PC = ActK->PC; PC != NULL; PC = PC->next)
         if (IsType(PC->Character, CHARACTER)) {
            for (PE = ActK->Effect; PE != NULL; PE = PE->next)
              AddOneCondRelation(PkPC, Pd, ActK, PC, PE);
            break;
         }

  PredNo = Pd->PredNo;
  Num = NumParaOfPred(PredNo) + Pd->NumEP;
  Para = (int *) calloc(Num, sizeof(int));

  // Predicate --> CEffect
  for (PE = Pd->CEffect; PE != NULL; PE = PE->next) {
    if (PE->Pred->VList.ParaIdx == PredNo) {
       for (i=0,Pt1=PE->Pred->next; Pt1 != NULL; i++,Pt1=Pt1->next)
         if (Pt1->VList.ParaIdx != i) break;

       if (Pt1 == NULL) continue;
    }

    law = (DomainLaw *) calloc(1, sizeof(DomainLaw));

    law->Step = 1;
    law->Flag = LAW0;
    law->Not1 = Pd->Type;
    law->Pred1 = CopyPredIntoTokenList(Pd);
    law->Not2 = PE->Type;
    law->Pred2 = CopyTokenList(PE->Pred);

    for (i = 0; i < Num; i++) Para[i] = NOFOUND;

    CopyVarParaOfPredIntoParaOfLaw(law, Pd);

    Pt = law->Para;
    for (i = 0; i < law->NumPara; i++,Pt++) Para[i] = Pt->VList.ParaIdx;

    IncreaseParaForLaw0_1(Para, law, Pd->Para, law->Pred2);

    GetPCListOfLaw(Para, law, Pd->Para, PkPC);

    TransDomainLaw(law); //PrintOneDomainLaw(law);

#ifdef TEST
    law->Index = (Law0==NULL ? 1 : 1+TLaw0->Index);
#endif
    if (Law0 == NULL) Law0 = law;
    else TLaw0->next = law;

    TLaw0 = law;

    i = law->Pred1->VList.ParaIdx;
    if (law->Not1!=law->Not2 && i==law->Pred2->VList.ParaIdx)
       (Predication+i)->Exclude = TRUE;
  }

  // Law: not CPC -\-> Predicate
  for (PC = Pd->CPC; PC != NULL; PC = PC->next) {
    if (IsClass(PC->PredNo, STATIC)) continue;

    law = (DomainLaw *) calloc(1, sizeof(DomainLaw));

    law->Step = 1;   law->Flag = LAW1;

    law->Not1 = (PC->Type != NOT);
    law->Pred1 = CopyPredIntoTokenList(PC);

    law->Not2 = (Pd->Type == NOT);
    law->Pred2 = CopyPredIntoTokenList(Pd);

    CopyVarParaOfPredIntoParaOfLaw(law, Pd);

    Pt = law->Para;
    for (i = 0; i < Num; i++) Para[i] = NOFOUND;
    for (i = 0; i < law->NumPara; i++,Pt++) Para[i] = Pt->VList.ParaIdx;

    IncreaseParaForLaw0_1(Para, law, Pd->Para, law->Pred1);

    GetPCListOfLaw(Para, law, Pd->Para, PkPC);

    TransDomainLaw(law); //PrintOneDomainLaw(law);

#ifdef TEST
    law->Index = (Law1==NULL ? 1 : 1+TLaw1->Index);
#endif
    if (Law1 == NULL) Law1 = law;
    else TLaw1->next = law;

    TLaw1 = law;
  }

  free(Para);
}

PCOfLaw *ppp(PCOfLaw *PC)
{
  PCOfLaw *PC1, *PC2, *PC3;

  PC1 = NULL;
  while (PC != NULL) {
    PC2 = (PCOfLaw *) calloc(1, sizeof(PCOfLaw));

    PC2->Not = PC->Not;
    PC2->Pred = CopyTokenList(PC->Pred);

    if (PC1 == NULL) PC1 = PC2;
    else PC3->next = PC2;

    PC3 = PC2;
  }

  return PC1;
}

//  Parent Predication
//           |
//           V
//PC:   (not PC) -\-> Pred
//		       |
//		       V
//law2:	         (not Pred) -\\-> Pred22
//		       | New Domain Law
//		       V
//law:       (not PC) -\\-> Pred22
void MakeOneIndirLaw(PredKnowledge *PC, int Num, TypedList *Para, DomainLaw *law2)
{
  DomainLaw *law;
  TokenList *Pt1;
  PCOfLaw   *PC1;
  int       i, *Para1;

  law = (DomainLaw *) calloc(1, sizeof(DomainLaw));

  law->Step = 1 + law2->Step;
  law->Flag = LAW2;

  law->PCLaw = ppp(law2->PCLaw);

  law->Not1 = (PC->Type != NOT);
  law->Pred1 = CopyPredIntoTokenList(PC);
  law->Not2 = law2->Not2;
  law->Pred2 = CopyTokenList(law2->Pred2);

  law->NumPara = law2->NumPara;
  law->Para = CopyTypedArray(law2->NumPara, law2->Para);

  Para1 = (int *) calloc(Num, sizeof(int));
  for (i = 0; i < Num; i++) Para1[i] = Para[i].VList.ParaIdx;

  Num = law->NumPara;
  for (Pt1 = law->Pred1->next; Pt1 != NULL; Pt1 = Pt1->next) {
    i = Pt1->VList.ParaIdx;
    if (IsConstant(i)) continue;

    if (Para1[i]!=NOFOUND && Para1[i]<Num) Pt1->VList.ParaIdx = Para1[i];
    else {
           Para1[i] = Pt1->VList.ParaIdx = Num++;
           IncreaseOneParaOfLaw(law, Para+i);
    }
  }

  free(Para1);

  TransDomainLaw(law);

  law->PC = PC1 = (PCOfLaw *) calloc(1, sizeof(PCOfLaw));
  PC1->Not = law2->Not1;
  PC1->Pred = CopyTokenList(law2->Pred1);
  PC1->next = CopyPCOfDomainLaw(law2);

  if (FindLawInListOfDomainLaw(law, Law1) != NULL) {
     FreeDomainOneLaw(law);
     return;
  }
//fprintf(Output, "\n"); PrintOneDomainLaw(law);

#ifdef TEST
  law->Index = 1+TLaw1->Index;
  law->Idx2 = law2->Index;
#endif

  TLaw1->next = law;
  TLaw1 = law;
}

//Para: New Parameters of law1
//        |
//        V
//law1: Pred11 --> Pred12
//		     |
//		     V
//law2:	           Pred21 -\\-> Pred22
//		     | New Domain Law
//		     V
//law:       Pred11 =\\=> Pred22
void MakeDomainAbsLaw(TypedList *Para, PredKnowledge *Pd, int Index, DomainLaw *law2)
{
  DomainLaw *law;
  TokenList *Pt;
  TypedList *Pt1;
  PCOfLaw   *PC;
  int       Num;

  law = (DomainLaw *) calloc(1, sizeof(DomainLaw));

  law->Step = 1 + law2->Step;
  law->Flag = LAW3;

  law->PCLaw = ppp(law2->PCLaw);

  law->Not1 = (Pd->Type==NOT);
  law->Pred1 = CopyPredIntoTokenList(Pd);

  law->Not2 = law2->Not2;
  law->Pred2 = CopyTokenList(law2->Pred2);

  law->NumPara = law2->NumPara;
  law->Para = CopyTypedArray(law2->NumPara, law2->Para);

  Num = law->NumPara;
  for (Pt = law->Pred1->next; Pt != NULL; Pt=Pt->next)
    if (!IsConstant(Pt->VList.ParaIdx)) {
       Pt1 = Para + Pt->VList.ParaIdx;
       if (Pt1->VList.ParaIdx != NOFOUND) Pt->VList.ParaIdx = Pt1->VList.ParaIdx;
       else {
              Pt1->VList.ParaIdx = Pt->VList.ParaIdx = Num++;
              IncreaseOneParaOfLaw(law, Pt1);
         }
    }

  TransDomainLaw(law);

  law->PC = PC = (PCOfLaw *) calloc(1, sizeof(PCOfLaw));
  PC->Not = !law2->Not1;
  PC->Pred = CopyTokenList(law2->Pred1);

  PC->next = CopyPCOfDomainLaw(law2);

#ifdef TEST
  law->Index = (Law3==NULL ? 1 : 1+TLaw3->Index);
  law->Idx1 = Index;
  law->Idx2 = law2->Index;
#endif

  if (FindLawInListOfDomainLaw(law, Law3) != NULL) FreeDomainOneLaw(law);
  else {
         if (Law3 == NULL) Law3 = law;
         else TLaw3->next = law;

         TLaw3 = law;
  }
}

Bool PCOfLawmatchsPCOfPKTree(int *iPara, PCOfLaw *PCLaw, TypedList *Para, PredKnowledge *PC)
{
  TypedList     *Para1, *Pt1;
  TokenList     *Pt2;
  PCOfLaw       *PC3;
  int           i, Idx1, Idx2, Num;

  if (PCLaw == NULL || PC == NULL) return TRUE;

  PC3 = PCLaw;
  while (PC3 != NULL) {
    Pt2 = PC3->Pred;

    while (PC != NULL) {
      if (PC->Type != PC3->Not || PC->PredNo != Pt2->VList.ParaIdx) {
         PC = PC->next;
         continue;
      }

      Para1 = PC->Para;
      for (Pt2 = Pt2->next; Pt2 != NULL; Para1++,Pt2=Pt2->next) {
        Idx1 = Para1->VList.ParaIdx;
        Idx2 = Pt2->VList.ParaIdx;

        if (IsConstant(Idx1) || IsConstant(Idx2)) {
           if (Idx1 != Idx2) break;
           continue;
        }

        if (Idx1 < Num) {
           Pt1 = Para + Idx2;
           if (Typing && !IsSame(Para1->Type->Name, Pt1->Type->Name)) break;

           i = iPara[Idx1];
           if (i == NOFOUND) iPara[Idx1] = Idx2;
           else if (i != Idx2) break;
        }
      }

      if (Pt2 == NULL) { PC = PC->next;  break; }
    }

    PC3 = PC3->next;
  }

  return TRUE;
}

PKTree *GetPredKnowledgeTree(PCOfLaw *PCLaw, Bool Not, TokenList *Pred, TypedList *Para)
{
  TypedList     *Para1, *Pt1;
  TokenList     *Pt2;
  PKTree        *Pk;
  Bool          Ok;
  int           i, Idx1, Idx2, Num, *iPara;

  Idx1 = Pred->VList.ParaIdx;
  Pk = (Not ? nPK : PK) + Idx1;

  for (Pk = Pk->next; Pk != NULL; Pk = Pk->next) {
//PrintPKTree(Pk);
    Num = NumParaOfPred(Idx1);
    iPara = (int *) calloc(Num, sizeof(int));

    for (i = 0; i < Num; i++) iPara[i] = NOFOUND;

    Para1 = Pk->Pred->Para;
    for (Pt2 = Pred->next; Pt2 != NULL; Para1++,Pt2=Pt2->next) {
      Idx1 = Para1->VList.ParaIdx;
      Idx2 = Pt2->VList.ParaIdx;

      if (IsConstant(Idx1) || IsConstant(Idx2)) {
         if (Idx1 != Idx2) break;
         continue;
      }

      Pt1 = Para + Idx2;
      if (Typing && !IsSame(Para1->Type->Name, Pt1->Type->Name)) break;

      i = iPara[Idx1];
      if (i == NOFOUND) iPara[Idx1] = Idx2;
      else if (i != Idx2) break;
    }

    Ok = FALSE;
    if (Pt2 == NULL) Ok = PCOfLawmatchsPCOfPKTree(iPara, PCLaw, Para, Pk->PC);

    free(iPara);

    if (Ok) break;
  }

  return Pk;
}

void MakeDomainIndirLaw(PredKnowledge *Pd, DomainLaw *law)
{
  PredKnowledge *PC;
  TypedList     *Pt, *Para;
  TokenList     *Pt1;
  PCOfLaw       *PC1;
  PENode        *PE;
  int           i, Num;

//fprintf(Output, "\n"); PrintOneDomainLaw(law);
//PrintPredication(12, Pd); fprintf(Output, "\n");

  Num = NumParaOfPred(Pd->PredNo) + Pd->NumEP;
  Pt = Para = CopyTypedArray(Num, Pd->Para);
  for (i = 0; i < Num; i++,Pt++) Pt->VList.ParaIdx = NOFOUND;

  Pt = Para;
  for (Pt1 = law->Pred1->next; Pt1 != NULL; Pt++,Pt1=Pt1->next)
    Pt->VList.ParaIdx = Pt1->VList.ParaIdx;

  for (PE = Pd->CEffect; PE != NULL; PE = PE->next) {
    for (PC1 = law->PC; PC1 != NULL; PC1 = PC1->next)
      if (EqualEffectAndPred(Para, PE->Pred, law->Para, PC1->Pred))
         break;

    if (PC1 != NULL ||
        EqualEffectAndPred(Para, PE->Pred, law->Para, law->Pred2)) {
       FreeTypedArray(Num, Para);
       return;
    }
  }

  for (PC = Pd->CPC; PC != NULL; PC = PC->next)
    if (!IsClass(PC->PredNo, STATIC) && PCInPCofDomainLaw(PC, Para, law)) {
       FreeTypedArray(Num, Para);
       return;
    }

  //law1: (not PC) -\-> Pd12
  //law:           (not Pd21) -\-> Pd22
  for (PC = Pd->CPC; PC != NULL; PC = PC->next)
    if (!IsClass(PC->PredNo, STATIC)) MakeOneIndirLaw(PC, Num, Para, law);

  FreeTypedArray(Num, Para);
}

void GenerateIndirectObsRelation(DomainLaw *law)
{
  PredKnowledge *PC;
  TypedList     *Pt, *Pt1;
  TokenList     *Pt2, *Para;
  PCOfLaw       *Pt3;
  PKTree        *Pk;
  int           i, Num, Idx1, Idx2, *PdPara;

//fprintf(Output, "\n"); PrintOneDomainLaw(law);
  if (law->PCLaw != NULL) {
     Bool *Flag;

     Flag = (Bool *) calloc(law->NumPara, sizeof(Bool));

     for (Pt2 = law->Pred1->next; Pt2 != NULL; Pt2 = Pt2->next) {
       i = Pt2->VList.ParaIdx;
       if (!IsConstant(i)) Flag[i] = TRUE;
     }

     for (Pt3 = law->PCLaw; Pt3 != NULL; Pt3 = Pt3->next) {
       for (Pt2 = Pt3->Pred->next; Pt2 != NULL; Pt2 = Pt2->next) {
         i = Pt2->VList.ParaIdx;
         if (!IsConstant(i) && Flag[i]) break;
       }

       if (Pt2 != NULL) break;
     }

     free(Flag);

     if (Pt3 == NULL) return;
  }

  Num = NumParaOfPred(law->Pred1->VList.ParaIdx);
  PdPara = (int *) calloc(Num, sizeof(int));
  for (i = 0; i < Num; i++) PdPara[i] = NOFOUND;

  i = 0;
  for (Pt2 = law->Pred1->next; Pt2 != NULL; Pt2 = Pt2->next)
    PdPara[i++] = Pt2->VList.ParaIdx;

  Pk = (law->Not1 ? PK : nPK) + law->Pred1->VList.ParaIdx;

  Pt3 = law->PCLaw;
  for (Pk = Pk->next; Pk != NULL; Pk = Pk->next) {
//PrintPKTree(Pk);
//PrintPredication(12, Pk->Pred); fprintf(Output, "\n");
    PC = Pk->PC;
    if ((PC!=NULL && Pt3==NULL) || (PC==NULL && Pt3!=NULL)) continue;

    if (PC != NULL) {
       Para = Pt3->Pred;
       if (PC->Type!=Pt3->Not || PC->PredNo!=Para->VList.ParaIdx) continue;

       Pt = PC->Para;
       for (Pt2 = law->PCLaw->Pred->next; Pt2 != NULL; Pt++,Pt2=Pt2->next) {
         Idx1 = Pt->VList.ParaIdx;
         Idx2 = Pt2->VList.ParaIdx;

         if (IsConstant(Idx1) || IsConstant(Idx2)) {
            if (Idx1 != Idx2) break;
         }
         else if (Idx1 >= Num || PdPara[Idx1] != Idx2) break;
       }

       if (Pt2 != NULL) continue;
    }

    Pt = Pk->Pred->Para;
    for (Pt2 = law->Pred1->next; Pt2 != NULL; Pt++,Pt2=Pt2->next) {
      Idx1 = Pt->VList.ParaIdx;
      Idx2 = Pt2->VList.ParaIdx;

      if (IsConstant(Idx1) || IsConstant(Idx2)) {
        if (Idx1 != Idx2) break;
      }
      else {
             Pt1 = law->Para + Idx2;
             if (Typing && !IsSame(Pt->Type->Name, Pt1->Type->Name))
                break;
      }
    }

    if (Pt2 == NULL) MakeDomainIndirLaw(Pk->Pred, law);
  }

  free(PdPara);
}

Bool CheckCharactericEffect(TypedList *Para, PredKnowledge *Pd, DomainLaw *law)
{
  PredKnowledge *PC;
  ActKnowledge  *ActK;
  TokenList     *Pt1, *Pt2;
  TypedList     *Pt3;
  PCOfLaw       *LPC, *LPC1;
  PENode        *PE;
  Bool          Equal;
  int           i, j, k, Num, *Para1;

  LPC = law->PC;
//for (LPC1 = LPC->next; LPC1 != NULL; LPC1 = LPC1->next) LPC = LPC1;
  for (LPC1 = LPC; LPC1 != NULL; LPC1 = LPC1->next) LPC = LPC1;

  if (LPC == NULL) return FALSE;

  for (ActK = Pd->Act; ActK != NULL; ActK = ActK->next) {
    PC = ActK->PC;
    while (!IsType(PC->Character, CHARACTER)) PC = PC->next;

    if ((PC->Type==NOT)!=LPC->Not || PC->PredNo!=LPC->Pred->VList.ParaIdx)
       continue;

    Num = NumParaOfAct(ActK->ActNo);
    Para1 = (int *) calloc(Num, sizeof(int));
    for (i = 0; i < Num; i++) Para1[i] = NOFOUND;

    Equal = TRUE;
    Pt3 = PC->Para;
    for (Pt1=LPC->Pred->next; Equal && Pt1!=NULL; Pt3++,Pt1=Pt1->next) {
      i = Pt3->VList.ParaIdx;
      j = (law->Para+Pt1->VList.ParaIdx)->VList.ParaIdx;

      if (IsConstant(i)) Equal = (i==j);
      else {
             k = (ActK->Para+i)->VList.ParaIdx;
             if (!IsExtraPara(k)) Equal = ((Para+i)->VList.ParaIdx==j);
             else if (Para1[i] == NOFOUND) Para1[i] = j;
                  else Equal = (Para1[i]==j);
      }
    }

    if (!Equal) { free(Para1);  continue; }

    for (PE = ActK->Effect; PE != NULL; PE = PE->next) {
      Equal = ((PE->Type==NOT)==law->Not2 && PE->Pred->VList.ParaIdx==law->Pred2->VList.ParaIdx);

      Pt1 = PE->Pred->next;
      Pt2 = law->Pred2->next;
      while (Equal && Pt1 != NULL) {
        i = Pt1->VList.ParaIdx;
        j = (law->Para+Pt2->VList.ParaIdx)->VList.ParaIdx;

        if (IsConstant(i)) Equal = (i==j);
        else {
               k = (ActK->Para+i)->VList.ParaIdx;
               if (!IsExtraPara(k)) Equal = ((Para+i)->VList.ParaIdx==j);
               else if (Para1[i] == NOFOUND) Para1[i] = j;
                    else Equal = (Para1[i]==j);
        }

        Pt1 = Pt1->next;  Pt2 = Pt2->next;
      }

      if (Equal) break;
    }

    free(Para1);

    if (Equal) return TRUE;
  }

  return FALSE;
}

//law1: Pred11 --> Pred12
//		     |
//		     V
//law2:	           Pred21 -\\-> Pred22
//		     | New Domain Law
//		     V
//           Pred11 =\\=> Pred22
void GenerateAbsolutionObsRelation(DomainLaw *law1, DomainLaw *law2)
{
  PredKnowledge *Pd;
  TypedList     *Para;
  TokenList     *Pt1, *Pt2;
  PCOfLaw       *PC;
  PENode        *PE;
  PKTree        *Pk;
  Bool          *Flag;
  int           i, idx1, idx2, Num;

  Num = law1->NumPara;
  Para = CopyTypedArray(Num, law1->Para);
  for (i = 0; i < Num; i++) Para[i].VList.ParaIdx = NOFOUND;

  Flag = (Bool *) calloc(law2->NumPara, sizeof(Bool));

  Pt2 = law2->Pred1->next;
  for (Pt1 = law1->Pred2->next; Pt1 != NULL; Pt1=Pt1->next,Pt2=Pt2->next) {
    idx1 = Pt1->VList.ParaIdx;
    idx2 = Pt2->VList.ParaIdx;

    if (IsConstant(idx1) || IsConstant(idx2)) {
       if (idx1 != idx2) break;
    }
    else {
           if (Typing && !IsSame((law1->Para+idx1)->Type->Name, (law2->Para+idx2)->Type->Name))
              break;

           (Para+idx1)->VList.ParaIdx = idx2;
           Flag[idx2] = TRUE;
    }
  }

  if (Pt1 != NULL) {
     FreeTypedArray(Num, Para);
     free(Flag);
     return;
  }

  if (law1->PCLaw != NULL) {
     Pt1 = law1->PCLaw->Pred->next;
     for (Pt2 = law2->PCLaw->Pred->next; Pt2 != NULL; Pt1=Pt1->next,Pt2=Pt2->next) {
       idx1 = Pt1->VList.ParaIdx;
       idx2 = Pt2->VList.ParaIdx;

       if (IsConstant(idx1) || IsConstant(idx2)) {
          if (idx1 != idx2) break;
       }
       else {
              idx2 = (Para+idx2)->VList.ParaIdx;
              if ((Flag[idx1] && idx1!=idx2) || (!Flag[idx1] && idx2!=NOFOUND))
                 break;
       }
     }

     if (Pt2 != NULL) {
        FreeTypedArray(Num, Para);
        free(Flag);
        return;
     }
  }

  Pk = GetPredKnowledgeTree(law1->PCLaw, law1->Not1, law1->Pred1, law1->Para);

//fprintf(Output, "\n"); PrintOneDomainLaw(law1);
//PrintPKTree(Pk);

  Pd = Pk->Pred;
  if (PCInPCofDomainLaw(Pd, Para, law2) ||
     (IsType(Pd->Character, CHARACTER) && law2->Not2 &&
      CheckCharactericEffect(Para, Pd, law2))) {
     FreeTypedArray(Num, Para);
     free(Flag);
     return;
  }

  for (PE = Pd->CEffect; PE != NULL; PE = PE->next) {
    if (EqualEffectAndPred(Para, PE->Pred, law2->Para, law2->Pred2)) break;

    for (PC = law2->PC; PC != NULL; PC = PC->next)
      if (EqualEffectAndPred(Para, PE->Pred, law2->Para, PC->Pred))
         break;

    if (PC != NULL) break;
  }

  if (PE == NULL) MakeDomainAbsLaw(Para, Pk->Pred, law1->Index, law2);

  FreeTypedArray(Num, Para);
  free(Flag);
}

DomainLaw *SortLawsOfDomain(DomainLaw *laws)
{
  DomainLaw *Pt, *Pt1, *Pt2, *Laws;
  PCOfLaw   *PC1, *PC2;
  Bool      Not;
  int       i;

  Laws = (DomainLaw *) calloc(NumPred, sizeof(DomainLaw));
  while (laws != NULL) {
    Pt = laws->next;

    Not = laws->Not1;  i = laws->Pred1->VList.ParaIdx;

    Pt1 = NULL;  Pt2 = (Laws+i)->next;
    if (Not)
       while (Pt2!=NULL && !Pt2->Not1) Pt1=Pt2,Pt2=Pt2->next;

    PC1 = laws->PCLaw;
    while (Pt2 != NULL && Pt2->Not1 == Not) {
      PC2 = Pt2->PCLaw;
      if ((PC1 != NULL && PC2 != NULL &&
           PC1->Pred->VList.ParaIdx == PC2->Pred->VList.ParaIdx) ||
          (PC1 == NULL && PC2 == NULL)) break;

      Pt1 = Pt2, Pt2 = Pt2->next;
    }

    while (Pt2 != NULL && Pt2->Not1 == Not) {
      PC2 = Pt2->PCLaw;
      if ((PC1 != NULL && PC2 != NULL &&
           PC1->Pred->VList.ParaIdx != PC2->Pred->VList.ParaIdx) ||
          (PC1 == NULL && PC2 == NULL)) break;

      Pt1 = Pt2, Pt2 = Pt2->next;
    }

    if (Pt1 != NULL) { laws->next = Pt1->next;  Pt1->next = laws; }
    else {
           laws->next = ((Laws+i)->next==NULL ? NULL : (Laws+i)->next);
           (Laws+i)->next = laws;
    }

    laws = Pt;
  }

  return Laws;
}

void SetMutexByCEffect(PredKnowledge *Pd, DomainLaw *law)
{
  TokenList *Pt1, *Pt2;
  PENode    *PE;
  Bool      Equal;
  int       i, Idx1, Idx2, Num, *Para;

  Num = NumParaOfPred(Pd->PredNo) + Pd->NumEP;
  Para = (int *) calloc(Num, sizeof(int));

  for (i = 0; i < Num; i++) Para[i] = NOFOUND;

  for (i=0,Pt1=law->Pred2->next; Pt1 != NULL; i++,Pt1=Pt1->next) {
    Idx1 = Pt1->VList.ParaIdx;
    if (!IsConstant(Idx1)) Para[i] = (law->Para+Idx1)->VList.ParaIdx;
  }

  for (PE = Pd->CEffect; PE != NULL; PE = PE->next) {
    Pt1 = PE->Pred;
    Pt2 = law->Pred1;
    if (law->Not1==(PE->Type==NOT) || Pt2->VList.ParaIdx!=Pt1->VList.ParaIdx)
       continue;

    Equal = TRUE;
    Pt1 = Pt1->next;    Pt2 = Pt2->next;
    while (Equal && Pt1!=NULL) {
      Idx1 = Pt1->VList.ParaIdx;
      Idx2 = Pt2->VList.ParaIdx;

      if (IsConstant(Idx1) || IsConstant(Idx2)) Equal = (Idx1==Idx2);
      else {
             Idx2 = (law->Para+Idx2)->VList.ParaIdx;
             if (Para[Idx1] == NOFOUND) Para[Idx1] = Idx2;
             else Equal = (Para[Idx1]==Idx2);
      }

      Pt1 = Pt1->next;  Pt2 = Pt2->next;
    }

    if (Equal) break;
  }

  free(Para);

  law->Mutex = (PE != NULL);
}

void SetMutexLaw(DomainLaw *law)
{
  PredKnowledge *Pd, *PC, *PC1;
  ActKnowledge  *ActK, *ActK1;
  TypedList     *Pt;
  TokenList     *Pt1;
  PENode        *PE, *PE1;
  PKTree        *Pk;
  Bool          Equal, Mutex1, Mutex2, Not;
  int           i, Idx1, Idx2, Num, *Para;

//fprintf(Output, "\n"); PrintOneDomainLaw(law);
  Pk = GetPredKnowledgeTree(law->PCLaw, !law->Not2, law->Pred2, law->Para);

  if (Pk == NULL) return;

  Pd = Pk->Pred;

  SetMutexByCEffect(Pd, law);

  if (law->Mutex || !law->Not2) return;

  Num = law->NumPara;
  Para = (int *) calloc(Num, sizeof(int));

  Mutex1 = FALSE;
  for (ActK = Pd->Act; ActK != NULL; ActK = ActK->next) {
    Mutex2 = TRUE;

    for (PC = ActK->PC; PC != NULL; PC = PC->next) {
      Not = (PC->Type == ATOM);

      if (PC->PredNo!=law->Pred1->VList.ParaIdx || Not==law->Not1) continue;

      for (i = 0; i < Num; i++) Para[i] = NOFOUND;

      Pt = Pd->Para;
      for (Pt1 = law->Pred2->next; Pt1 != NULL; Pt1 = Pt1->next)
        if (!IsConstant(Pt1->VList.ParaIdx)) Para[Pt1->VList.ParaIdx] = Pt->VList.ParaIdx;

      Equal = TRUE;
      Pt = PC->Para;  Pt1 = law->Pred1->next;
      while (Equal && Pt1 != NULL) {
        Idx1 = Pt->VList.ParaIdx;
        if (!IsConstant(Idx1)) Idx1 = (ActK->Para+Idx1)->VList.ParaIdx;

        Idx2 = Pt1->VList.ParaIdx;

        if (Para[Idx2] == NOFOUND) Para[Idx2] = Idx1;
        else Equal = (Para[Idx2]==Idx1);

        Pt++;  Pt1 = Pt1->next;
      }

      if (!Equal) continue;

      Mutex2 = FALSE;

      for (PE = ActK->Effect; PE != NULL; PE = PE->next) {
        if (PC->PredNo != PE->Pred->VList.ParaIdx ||
           Not == (PE->Type==ATOM)) continue;

        Pt = PC->Para;
        for (Pt1 = PE->Pred->next; Pt1 != NULL; Pt++,Pt1=Pt1->next)
          if (Pt->VList.ParaIdx != Pt1->VList.ParaIdx) break;

        if (Pt1 == NULL) break;
      }

      if (PE != NULL) { Mutex2 = TRUE;  break; }
    }

    if (!Mutex2) { Mutex1 = FALSE;  break; }

    if (!Mutex1 && PC != NULL) {
       Mutex1 = TRUE;
       ActK1 = ActK, PC1 = PC, PE1 = PE;
    }
  }

  free(Para);

  if (Mutex1) {
     law->Mutex = TRUE;
     law = AddOneCondRelation(Pk->PC, Pd, ActK1, PC1, PE1);
     law->Mutex = TRUE;
  }
}

Bool UniformTwoPreds(int Num, int *Para, TokenList *Pd2, TypedList *Pd1)
{
  int i, j;

  while (Pd2 != NULL) {
    i = Pd1->VList.ParaIdx;
    j = Pd2->VList.ParaIdx;

    if (IsConstant(i)) {
       if (i != j) return FALSE;
    }
    else {
           if (Para[i] == NOFOUND) {
              if (!CheckTransform(Num, Para, i, j)) return FALSE;
           }
           else if (Para[i] != j) return FALSE;
        }

    Pd1++;  Pd2 = Pd2->next;
  }

  return TRUE;
}

Bool CheckDomainLaw(DomainLaw *LAW, int Num, int *Para, PredKnowledge *Pd1, PredKnowledge *Pd2)
{
  DomainLaw *law;
  Bool      Not1, Not2;
  int       i;

  for (law = (LAW+Pd1->PredNo)->next; law != NULL; law = law->next) {
    Not1 = (Pd1->Type == NOT);
    Not2 = (Pd2->Type == NOT);
    if (Not1 != law->Not1 || Not2 != law->Not2 ||
        Pd2->PredNo != law->Pred2->VList.ParaIdx) continue;

    for (i = 0; i < Num; i++) Para[i] = NOFOUND;

    if (UniformTwoPreds(Num, Para, law->Pred1->next, Pd1->Para) &&
        UniformTwoPreds(Num, Para, law->Pred2->next, Pd2->Para)) break;
  }

  return (law != NULL);
}

void SortPCOfActKnowledgeByLaw(ActKnowledge *ActK)
{
  PredKnowledge *PC, *PC1, *PC2, *PC3, *PC4, *PC5;
  TypeOfPred    TypeOfPd;
  int           Num, *Para;

  PC = ActK->PC;
  if (PC == NULL) return;

  PC1 = PC2 = PC3 = PC4 = NULL;
  while (PC != NULL) {
    TypeOfPd = ClassOfPred(PC->PredNo);

    if (TypeOfPd == STATIC ||
        (PC->Type==ATOM && TypeOfPd==DESCENDING) ||
        (PC->Type==NOT && TypeOfPd==ASCENDING)) {
       if (PC1 == NULL) PC1 = PC;
       else PC2->next = PC;
       PC2 = PC;
    }
    else {
           if (PC3 == NULL) PC3 = PC;
           else PC4->next = PC;
           PC4 = PC;
    }
    PC = PC->next;
  }

  if (PC4 != NULL) PC4->next = NULL;

  if (PC3 == NULL) return;

  Num = NumParaOfAct(ActK->ActNo);
  Para = (int *) calloc(Num, sizeof(int));

  while (PC3->next != NULL) {
    PC4 = PC3;
    while (PC4->next != NULL) {
      PC5 = PC4->next;
      if (!CheckDomainLaw(Law0, Num, Para, PC5, PC3) &&
          !CheckDomainLaw(Law3, Num, Para, PC3, PC5))
         PC4 = PC4->next;
      else {
             PC4->next = PC5->next;
             PC5->next = PC3;

             PC3 = PC5;
      }
    }

    if (PC1 == NULL) PC1 = PC3;
    else PC2->next = PC3;
    PC2 = PC3;

    PC3 = PC3->next;
  }

  if (PC1 == NULL) PC1 = PC3;
  else PC2->next = PC3;

  ActK->PC = PC1;

  free(Para);
}

// PC --> (not PC1), PC1 --> (not PC)
Bool CheckTwoPredsForMutex(int *Para, PredKnowledge *PC, ActKnowledge *ActK, PredKnowledge *PC1)
{
  DomainLaw *law;
  TokenList *Pt1;
  TypedList *Pt2;
  int       i, j, Num, *Para1, *Para2;

  Num = NumParaOfPred(PC->PredNo) + NumParaOfPred(PC1->PredNo);
  Para1 = (int *) calloc(Num, sizeof(int));

  for (law = (Law0+PC->PredNo)->next; law != NULL; law = law->next)
    if (law->Mutex && law->Not1 == PC->Type &&
        law->Not2 != PC1->Type && law->Pred2->VList.ParaIdx == PC1->PredNo) {
       for (i = 0; i < Num; i++) Para1[i] = NOFOUND;

       Para2 = Para;
       for (Pt1 = law->Pred1->next; Pt1 != NULL; Para2++,Pt1=Pt1->next) {
         i = Pt1->VList.ParaIdx;
         j = *Para2;
         if (!IsConstant(i) && !IsConstant(j)) Para1[i] = j;
         else if (i != j) break;
       }

       if (Pt1 != NULL) continue;

       Pt2 = PC1->Para;
       for (Pt1 = law->Pred2->next; Pt1 != NULL; Pt2++,Pt1=Pt1->next) {
         i = Pt1->VList.ParaIdx;
         j = Pt2->VList.ParaIdx;
         if (IsConstant(i) || IsConstant(j)) {
            if (i != j) break;
         }
         else {
                j = (ActK->Para+j)->VList.ParaIdx;
                if (Para1[i] == NOFOUND) Para1[i] = j;
                else if (Para1[i] != j) break;
         }
       }

       if (Pt1 == NULL) break;
    }

  free(Para1);
  return (law != NULL);
}

Bool SetMutexRelation(PredKnowledge *PC, int *Para, ActKnowledge *ActK)
{
  PredKnowledge *PC1;
  int           i, j, Num, Num1;

  Num = NumParaOfPred(PC->PredNo);
  for (; ActK != NULL; ActK = ActK->next)
    for (PC1 = ActK->PC; PC1 != NULL; PC1 = PC1->next) {
      if (IsEqual(PC1->PredNo)) continue;

      // PC1 == PC or PC1 == (not PC) ??
      if (PC1->PredNo == PC->PredNo) {
         for (i = 0; i < Num; i++) {
           j = (PC1->Para+i)->VList.ParaIdx;

           if (!IsConstant(j)) j = (ActK->Para+j)->VList.ParaIdx;

           if (j != Para[i]) break;
         }

         if (i >= Num) continue;
      }

      Num1 = NumParaOfPred(PC1->PredNo);
      for (i = 0; i< Num1; i++) {
        j = (PC1->Para+i)->VList.ParaIdx;

        if (!IsConstant(j)) {
           j = (ActK->Para+j)->VList.ParaIdx;
           if (IsExtraPara(j)) break;
        }
      }

      if (i >= Num1 && CheckTwoPredsForMutex(Para, PC, ActK, PC1)) {
         PC->Character |= MUTEX;
         PC1->Character |= MUTEX;
         break;
      }
    }

  return IsType(PC->Character, MUTEX);
}

void SetMutexRelationOfPC(PredKnowledge *Pd)
{
  PredKnowledge *PC;
  ActKnowledge  *ActK;
  Bool          Ok;
  int           i, j, Num, *Para;

  for (ActK = Pd->Act; ActK != NULL; ActK = ActK->next)
    for (PC = ActK->PC; PC != NULL; PC = PC->next)
      if (PC->NumNonValue > 0) {
         // Set MAINPC into PC of action
         Num = NumParaOfPred(PC->PredNo);
         Para = (int *) calloc(Num, sizeof(int));
         for (i = 0; i < Num; i++) Para[i] = (Pd->Para+i)->VList.ParaIdx;

         if (CheckTwoPredsForMutex(Para, Pd, ActK, PC)) {
            PC->Character |= MAINPC;
            Pd->Character |= MAINPC;
         }

         free(Para);
      }

//PrintPredication(12, Pd); fprintf(Output, "\n");
  if (NonMainPC(Pd->Character) || Pd->NumAct < 2) return;

  for (ActK = Pd->Act; ActK->next != NULL; ActK = ActK->next)
    for (PC = ActK->PC; PC != NULL; PC = PC->next) {
      if (PC->Character != NONE) continue;

      Num = NumParaOfPred(PC->PredNo);
      Para = (int *) calloc(Num, sizeof(int));
      for (i = 0; i < Num; i++) {
        j = (PC->Para+i)->VList.ParaIdx;
        if (IsConstant(j)) Para[i] = j;
        else {
               j = (ActK->Para+j)->VList.ParaIdx;
               if (IsExtraPara(j)) break;
               Para[i] = j;
        }
      }

      Ok = FALSE;
      if (i >= Num) Ok = SetMutexRelation(PC, Para, ActK->next);

      free(Para);
      if (Ok) {
         Pd->Character |= MUTEX;
         break;
      }
    }
}

void GetDomainLaw()
{
  ActKnowledge *ActK;
  TypeOfPred   TypeOfPd;
  DomainLaw    *law, *law1;
  PCOfLaw      *Pt, *Pt1;
  PKTree       *Pk,*Pk1, *Pk2;
  int	       i;

//PrintKnowledgeTree();
  Law0 = Law1 = NULL;
  for (i = 0; i < NumPred; i++) {
    for (Pk=(PK+i)->next; Pk!=NULL; Pk=Pk->next) GetDomainBasicLaw(Pk);
    for (Pk=(nPK+i)->next; Pk!=NULL; Pk=Pk->next) GetDomainBasicLaw(Pk);
  }

//PrintDomainLawList(Law0, "Concomitancy");
  for (law = Law0; law != NULL; law = law->next)
    if (law->Flag == LAW0) SetMutexLaw(law);
//PrintDomainLawList(Law0, "Concomitancy");

//PrintDomainLawList(Law1, "Direct Obstructive");
  for (law = Law1; law != NULL; law = law->next)  // LAW2 = LAW1 + LAW1(LAW2)
    GenerateIndirectObsRelation(law);
//PrintDomainLawList(Law1, "Indirect Obstructive");

  Law3 = NULL;
  for (law = Law1; law != NULL; law = law->next)  // LAW3 = LAW0(LAW01) + LAW1(LAW2)
    for (law1 = Law0; law1 != NULL; law1 = law1->next) {
      Pt = law->PCLaw;
      Pt1 = law1->PCLaw;

      if (law1->Not2 != law->Not1 ||
          law1->Pred2->VList.ParaIdx != law->Pred1->VList.ParaIdx ||
          (Pt == NULL && Pt1 != NULL) || (Pt != NULL && Pt1 == NULL))
         continue;

      // law1: Pd1 --> Pd2
      //  law:         Pd2 -\\-> Pd3
#ifdef NEWABS
      TypeOfPd = ClassOfPred(law1->Pred2->VList.ParaIdx);
      if (law1->Mutex || (law1->Not2==NOT && TypeOfPd==DESCENDING)
                      || (law1->Not2==ATOM && TypeOfPd==ASCENDING))
#endif
         GenerateAbsolutionObsRelation(law1, law);
    }
//PrintDomainLawList(Law0, "Concomitancy/Cond-Concomitancy");
//PrintDomainLawList(Law1, "Direct Obstructive");
//PrintDomainLawList(Law3, "Absolute Obstructive");

  NumLaw0 = (TLaw0==NULL ? 0: TLaw0->Index);
  NumLaw1 = (TLaw1==NULL ? 0: TLaw1->Index);
  NumLaw3 = (TLaw3==NULL ? 0: TLaw3->Index);

  Law0 = SortLawsOfDomain(Law0);
  Law1 = SortLawsOfDomain(Law1);
  Law3 = SortLawsOfDomain(Law3);

  if (DispLaw) {
     PrintLawsOfDomain("Concomitancy/Cond-Concomitancy", NumLaw0, Law0);
     PrintLawsOfDomain("Obstructive", NumLaw1, Law1);
     PrintLawsOfDomain("Absolute Obstructive", NumLaw3, Law3);
  }

//PrintKnowledgeTree();
  // Sort PCs of Action
  Pk1 = PK;   Pk2 = nPK;
  for (i = 0; i < NumPred; i++,Pk1++,Pk2++) {
    for (Pk = Pk1->next; Pk != NULL; Pk = Pk->next)
      for (ActK = Pk->Pred->Act; ActK != NULL; ActK = ActK->next)
        SortPCOfActKnowledgeByLaw(ActK);

    for (Pk = Pk2->next; Pk != NULL; Pk = Pk->next)
      for (ActK = Pk->Pred->Act; ActK != NULL; ActK = ActK->next)
        SortPCOfActKnowledgeByLaw(ActK);
  }
  // End

//PrintKnowledgeTree();
  Pk1 = PK;   Pk2 = nPK;
  for (i = 0; i < NumPred; i++,Pk1++,Pk2++) {
    for (Pk = Pk1->next; Pk != NULL; Pk = Pk->next)
      SetMutexRelationOfPC(Pk->Pred);

    for (Pk = Pk2->next; Pk != NULL; Pk = Pk->next)
      SetMutexRelationOfPC(Pk->Pred);
  }

//PrintDomain();  PrintKnowledgeTree();  //ModifyTreeOfAction();
}
